/*
 * Results.cuh
 *
 *  Created on: Sep 5, 2013
 *      Author: jaime
 */

#ifndef RESULTS_CUH_
#define RESULTS_CUH_

#include "SATSolver.cuh"
#include <vector>
using namespace std;

class Results {
public:
	Results(int number_of_vars, bool on_gpu);
	__device__ void set_satisfiable_results(Lit* results, int size);
	__host__ __device__ void set_undef();
	__host__ void set_host_status(sat_status status);
	__host__ void print_results(vector <Lit> & set_literals);
	__host__ sat_status get_status();
private:
	/**
	 * Results stored as sat_status rather than literals to allow having undefined literals!
	 */
	sat_status* results_dev;
	sat_status* formula_status_dev;
	sat_status formula_status_host;
	int number_of_vars;
	bool on_gpu;

	__host__ void print_sat_results(vector <Lit> & set_literals);
};

#endif /* RESULTS_CUH_ */
